Nuprl Lemma : ds_property
11,40
postcript
pdf
A
:Type,
d
:DS(
A
),
a
:
A
,
x
,
y
:dstype(
A
;
d
;
a
). {(
x
=
y
)
(
x
=
y
)}
latex
Definitions
x
:
A
.
B
(
x
)
,
{
T
}
,
x
=
y
,
dseq(
d
;
a
)
,
t
T
,
dstype(
TypeNames
;
d
;
a
)
,
t
.2
,
t
.1
,
DS(
A
)
Lemmas
deq
property
,
dstype
wf
,
discrete
struct
wf
origin
A:Type, d:DS(A), a:A, x, y:dstype(A; d; a). {(x = y) 
(
x = y)} A:Type, d:DS(A), a:A, x, y:dstype(A; d; a). {(x = y) (x = y)} x:A. B(x)
T